Formal verification, especially error detection, is rapidly increasing in importance with the rising complexity of designs. A typical constraint in verification is the total amount of resources available, including time and memory. Satisfiability (SAT)-based bounded model checking (BMC) approaches are often a preferred method for detecting error states that are not very deep. However, these techniques can become quite expensive when many time-frames are required to be tested. Binary Decision Diagram (BDD) based approaches are better choices for those deep cases where the image BDDs remain moderately small, as constructing large BDDs for many image steps can be very expensive.